{-# LANGUAGE TypeFamilies, QuasiQuotes, TypeOperators, ScopedTypeVariables,
  GADTs #-}

{- |

Module      :  Type.Yoko.BTree
Copyright   :  (c) The University of Kansas 2011
License     :  BSD3

Maintainer  :  nicolas.frisby@gmail.com
Stability   :  experimental
Portability :  see LANGUAGE pragmas (... GHC)

The @Finite@ type-class provides default implementations for type sets whose
members can be enumerated via ':=:' and ':||'.

-}

module Type.Yoko.BTree where

import Type.Yoko.Type
import Type.Yoko.SetModel
import Type.Yoko.Natural








finiteNP :: Finite u => NP u f -> NP (Fin u) f
finiteNP = firstNP toFin


type instance Fin ((:=:) t) = ((:=:) t)
instance Finite ((:=:) t) where toFin = id; predFin _ _ x = x
instance Etinif ((:=:) t) where frFin = id

type instance Fin (u :|| v) = Fin u :|| Fin v
instance (Finite u, Finite v) => Finite (u :|| v) where
  toFin (LeftU u) = LeftU $ toFin u
  toFin (RightU u) = predFin [qP|u :: *->*|] (elemProxy u) $ RightU $ toFin u
  predFin _ pT x = predFin [qP|u :: *->*|] pT $ predFin [qP|v :: *->*|] pT x
instance (Etinif u, Etinif v) => Etinif (u :|| v) where
  frFin (LeftU u) = LeftU $ frFin u
  frFin (RightU u) = predFin [qP|u :: *->*|] (elemProxy u) $ RightU $ frFin u



{-
-- | @Norm@ uses @NormW@ to remove duplicates from (i.e. /normalize/) a
-- type-sum.
type family Norm c
type instance Norm V = V
type instance Norm (N t) = N t
type instance Norm (ts :+ us) = NormW (ts :+ us) V

-- | @NormW@ combines two type-sums into a right-associated type-sum containing
-- no duplicates.
type family NormW c acc
type instance NormW V acc = acc
type instance NormW (N t) acc = If (Elem t acc) acc (N t :+ acc)
type instance NormW (ts :+ us) acc = NormW ts (NormW us acc)
-}





one :: Unwrap f t -> NT ((:=:) t) f
one x = constNT infP x

oneF :: Wrapper f => f t -> NT ((:=:) t) f
oneF = one . unwrap

infixr 6 |||, .|.
both, (|||) :: NT u f -> NT v f -> NT (u :|| v) f
both f g = orNT f g; (|||) = both

infixl 5 ||.; infixr 5 .||
(.|.) :: Wrapper f => Unwrap f t -> Unwrap f s -> NT ((:=:) t :|| (:=:) s) f
(||.) :: Wrapper f => NT ts f -> Unwrap f t -> NT (ts :|| (:=:) t) f
(.||) :: Wrapper f => Unwrap f t -> NT ts f -> NT ((:=:) t :|| ts) f
f .|. g = one f ||| one g; f ||. g = f ||| one g; f .|| g = one f ||| g
